Markov Automata: Deciding Weak Bisimulation by means of non-naively Vanishing States

摘要

This paper develops a decision algorithm for weak bisimulation on MarkovAutomata (MA). For that purpose, different notions of vanishing state (aconcept known from the area of Generalised Stochastic Petri Nets) are defined.Vanishing states are shown to be essential for relating the concepts of(state-based) naive weak bisimulation and (distribution-based) weakbisimulation. The bisimulation algorithm presented here follows thepartition-refinement scheme and has exponential time complexity.